FDL - Nuprl Lemma : rel-immediate_functionality_wrt_iff

Nuprl Lemma : rel-immediate_functionality_wrt_iff

T:Type, R, Q:(T

T

).
(

x, y:T. (R(x,y))

(Q(x,y)))

(

x, y:T. (R!(x,y))

(Q!(x,y)))

Definitions R!, False, P Q, Void, A c B, P Q, P Q, A, x:A. B(x), P & Q, , x:A B(x), f(a), x:AB(x), Type, t T, x. t(x), x.A(x)

Lemmas and functionality wrt iff, not functionality wrt iff, all functionality wrt iff, not wf